CPAchecker Report

/* service_maxrgb_cpu.c */  
  
/* service_maxrgb.h */  
  
#ifndef __SERVICE_MAXRGB_H__  
#define __SERVICE_MAXRGB_H__  
  
/* service_plugin.h */  
  
#ifndef __SERVICE_PLUGIN_H__  
#define __SERVICE_PLUGIN_H__  
  
#include <stdint.h>  
  
#define QuantumRange UINT16_MAX  
  
typedef uint16_t Quantum;  
  
typedef struct __PixelPacket__ {  
	Quantum blue;  
	Quantum green;  
	Quantum red;  
	Quantum opacity;  
} PixelPacket;  
  
typedef struct __Image__ {  
	PixelPacket *image;  
	int32_t rows;  
	int32_t columns;  
	int64_t j_arr;  
} Image;  
  
void run_service(char resource, void *handler_gpu, Image **target_images, int32_t *target_images_size, Image *source_images, int32_t source_images_size, double *params, int32_t *status_code);  
  
void get_service_ids(char ***id_strings, int32_t *id_strings_size);  
void get_service_info(char ***info_strings, int32_t *info_strings_size);  
void get_service_params(char ***param_strings, int32_t *param_strings_size);  
void get_service_resources(char ***resource_strings, int32_t *resource_strings_size);  
int32_t get_number_of_input_images(void);  
int32_t get_number_of_output_images(void);  
  
#endif /* __SERVICE_PLUGIN_H__ */  
/* common.h */  
  
#ifndef __COMMON_H__  
#define __COMMON_H__  
  
#include <stdio.h>  
  
void malloc_copy_string_array(char ***target_array, char **source_array, int32_t array_size);  
void free_string_array(char ***array, int32_t array_size);  
  
#endif /* __COMMON_H__ */  
  
#include <stdio.h>  
  
int32_t run_service_maxrgb_scpu(PixelPacket *pixpack_target, PixelPacket *pixpack_source, int32_t rows, int32_t columns, int32_t mode);  
int32_t run_service_maxrgb_cpu(PixelPacket *pixpack_target, PixelPacket *pixpack_source, int32_t rows, int32_t columns, int32_t mode);  
int32_t run_service_maxrgb_gpu(PixelPacket *pixpack_target, PixelPacket *pixpack_source, int32_t rows, int32_t columns, int32_t mode);  
int32_t run_service_maxrgb_fpga(PixelPacket *pixpack_target, PixelPacket *pixpack_source, int32_t rows, int32_t columns, int32_t mode);  
  
// internal maxfile interface(s)  
void run_service_max_maxrgb(uint16_t *dataOut, uint16_t *dataIn, uint32_t picSize, uint32_t mode);  
	  
#endif /* __SERVICE_MAXRGB_H__ */  
  
int32_t run_service_maxrgb_cpu(PixelPacket *pixpack_target, PixelPacket *pixpack_source, int32_t rows, int32_t columns, int32_t mode) {  
	int32_t i, j, pos;  
  
	/**  
	  * Modes:  
	  * 1: maxRGB  
	  * 2: minRGB  
	  * 3: max increase  
	  * 4: min erase  
	**/  
  
	if ((mode == 1) || (mode == 3)) {  
		#pragma omp parallel  
		{  
			#pragma omp for private(j, pos)  
			for (i = 0; i < rows; ++i) {  
				for (j = 0; j < columns; ++j) {  
					pos = i * columns + j;  
  
					//check if color is grey  
					if ((pixpack_source[pos].red == pixpack_source[pos].green) && (pixpack_source[pos].red == pixpack_source[pos].blue)) {  
						pixpack_target[pos].red	  = pixpack_source[pos].red;  
						pixpack_target[pos].green = pixpack_source[pos].green;  
						pixpack_target[pos].blue  = pixpack_source[pos].blue;  
						continue;  
					}  
  
  
					uint16_t *maxPtr;  
					maxPtr = &pixpack_source[pos].blue;  
					uint16_t *colorPtr;  
					colorPtr = &pixpack_source[pos].blue;  
					int8_t c;  
  
					for (c = 1; c < 3; c++) {  
						colorPtr++;  
						if (*colorPtr > *maxPtr)  
							maxPtr = colorPtr;  
					}  
  
					uint16_t *colorPtrSource;  
					colorPtrSource = &pixpack_source[pos].blue;  
					uint16_t *colorPtrTarget;  
					colorPtrTarget = &pixpack_target[pos].blue;  
  
					switch (mode) {  
						case 1:  
							for (c = 0; c < 3; c++) {  
								if (colorPtrSource == maxPtr)  
									*colorPtrTarget = *colorPtrSource;  
								else  
									*colorPtrTarget = 0;  
  
								colorPtrSource++;  
								colorPtrTarget++;  
							}  
							break;  
						case 3:  
							for (c = 0; c < 3; c++) {  
								if (colorPtrSource == maxPtr)  
									*colorPtrTarget = 65535;  
								else  
									*colorPtrTarget = *colorPtrSource;  
  
								colorPtrSource++;  
								colorPtrTarget++;  
							}  
					}  
				}  
			}  
		}  
	} else if ((mode == 2) || (mode == 4)) {  
		#pragma omp parallel  
		{  
			#pragma omp for private(j, pos)  
			for (i = 0; i < rows; ++i) {  
				for (j = 0; j < columns; ++j) {  
					pos = i * columns + j;  
  
					//check if color is grey  
					if ((pixpack_source[pos].red == pixpack_source[pos].green) && (pixpack_source[pos].red == pixpack_source[pos].blue)) {  
						pixpack_target[pos].red	  = pixpack_source[pos].red;  
						pixpack_target[pos].green = pixpack_source[pos].green;  
						pixpack_target[pos].blue  = pixpack_source[pos].blue;  
						continue;  
					}  
  
  
					uint16_t *minPtr;  
					minPtr = &pixpack_source[pos].blue;  
					uint16_t *colorPtr;  
					colorPtr = &pixpack_source[pos].blue;  
					int8_t c;  
  
					for (c = 1; c < 3; c++) {  
						colorPtr++;  
						if (*colorPtr < *minPtr)  
							minPtr = colorPtr;  
					}  
  
					uint16_t *colorPtrSource;  
					colorPtrSource = &pixpack_source[pos].blue;  
					uint16_t *colorPtrTarget;  
					colorPtrTarget = &pixpack_target[pos].blue;  
  
					switch (mode) {  
						case 2:  
							for (c = 0; c < 3; c++) {  
								if (colorPtrSource == minPtr)  
									*colorPtrTarget = *colorPtrSource;  
								else  
									*colorPtrTarget = 0;  
  
								colorPtrSource++;  
								colorPtrTarget++;  
							}  
							break;  
						case 4:  
							for (c = 0; c < 3; c++) {  
								if (colorPtrSource == minPtr)  
									*colorPtrTarget = 0;  
								else  
									*colorPtrTarget = *colorPtrSource;  
  
								colorPtrSource++;  
								colorPtrTarget++;  
							}  
					}  
				}  
			}  
		}  
	}  
	return 0;  
}  

2018-06-07 17:03:15:512	INFO	ResourceLimitChecker.fromConfiguration	Using the following resource limits: CPU-time limit of 900s

2018-06-07 17:03:15:793	INFO	CPAchecker.run	CPAchecker 1.7 (Java HotSpot(TM) 64-Bit Server VM 1.8.0_91) started

2018-06-07 17:03:19:170	WARNING	ARGCPA:FormulaManagerView.<init>	Using unsound approximation of ints with unbounded integers and floats with unbounded integers for encoding program semantics.

2018-06-07 17:03:19:279	INFO	CPAchecker.runAlgorithm	Starting analysis ...

2018-06-07 17:13:55:854	WARNING	ShutdownNotifier.shutdownIfNecessary	Warning: Analysis interrupted (The JVM is shutting down, probably because Ctrl+C was pressed.)

2018-06-07 17:13:55:859	SEVERE	ProofGenerator.generateProof	Proof cannot be generated because checked property not known to be true.

2018-06-07 17:14:09:925	WARNING	StatisticsUtils.writeOutputFiles	Writing output files from org.sosy_lab.cpachecker.cpa.arg.ARGStatistics took    14.039s.

AutomatonAnalysis (AssertionAutomaton) statistics

-------------------------------------------------

Number of states:                                  1

Total time for successor computation:                  1.173s

  Time for transition matches:                         0.507s

  Time for transition assertions:                      0.000s

  Time for transition actions:                         0.000s

Automaton transfers with branching:                0

Automaton transfer successors:                        59461 (count: 59461, min: 1, max: 1, avg: 1.00) [1 x 59461]

AutomatonAnalysis (ErrorLabelAutomaton) statistics

--------------------------------------------------

Number of states:                                  1

Total time for successor computation:                  0.523s

  Time for transition matches:                         0.198s

  Time for transition assertions:                      0.000s

  Time for transition actions:                         0.000s

Automaton transfers with branching:                0

Automaton transfer successors:                        59461 (count: 59461, min: 1, max: 1, avg: 1.00) [1 x 59461]

AutomatonAnalysis (TerminatingFunctions) statistics

---------------------------------------------------

Number of states:                                  1

Total time for successor computation:                  0.513s

  Time for transition matches:                         0.169s

  Time for transition assertions:                      0.000s

  Time for transition actions:                         0.000s

Automaton transfers with branching:                0

Automaton transfer successors:                        59461 (count: 59461, min: 1, max: 1, avg: 1.00) [1 x 59461]

CPA algorithm statistics

------------------------

Number of iterations:            52056

Max size of waitlist:            6

Average size of waitlist:        5

Number of computed successors:   59461

Max successors for one state:    2

Number of times merged:          0

Number of times stopped:         7401

Number of times breaked:         0

Total time for CPA algorithm:       636.558s (Max:   636.558s)

  Time for choose from waitlist:      0.284s

  Time for precision adjustment:      1.027s

  Time for transfer relation:         5.504s

  Time for merge operator:          388.203s

  Time for stop operator:           238.075s

  Time for adding to reached set:     0.899s

CPAchecker general statistics

-----------------------------

Number of program locations:     399

Number of CFA edges:             426

Number of relevant variables:    18

Number of functions:             1

Number of loops:                 10

Size of reached set:             52060

  Number of reached locations:   258 (65%)

    Avg states per location:     201

    Max states per location:     7401 (at node N92)

  Number of reached functions:   1 (100%)

  Number of partitions:          258

    Avg size of partitions:      201

    Max size of partitions:      7401 (with key [N92 (before line 142), Function run_service_maxrgb_cpu called from node N1, stack depth 1 [2974f221], stack [run_service_maxrgb_cpu]])

  Number of target states:       0

  Size of final wait list        5

Time for analysis setup:          3.470s

  Time for loading CPAs:          1.271s

  Time for loading parser:        0.607s

  Time for CFA construction:      1.479s

    Time for parsing file(s):     0.530s

    Time for AST to CFA:          0.351s

    Time for CFA sanity check:    0.055s

    Time for post-processing:     0.326s

      Time for var class.:        0.209s

        Time for collecting variables:                 0.060s

        Time for solving dependencies:                 0.001s

        Time for building hierarchy:                   0.000s

        Time for building classification:              0.109s

        Time for exporting data:                       0.016s

    Time for CFA export:          0.220s

Time for Analysis:              636.571s

CPU time for analysis:          648.730s

Total time for CPAchecker:      640.045s

Total CPU time for CPAchecker:  653.390s

Time for statistics:             14.288s

Time for Garbage Collector:       6.011s (in 1105 runs)

Garbage Collector(s) used:    PS MarkSweep, PS Scavenge

Used heap memory:                473MB (   451 MiB) max;    226MB (   215 MiB) avg;    621MB (   592 MiB) peak

Used non-heap memory:             32MB (    31 MiB) max;     30MB (    29 MiB) avg;     38MB (    36 MiB) peak

Used in PS Old Gen pool:          55MB (    52 MiB) max;     40MB (    38 MiB) avg;    162MB (   154 MiB) peak

Allocated heap memory:           485MB (   463 MiB) max;    423MB (   404 MiB) avg

Allocated non-heap memory:        34MB (    33 MiB) max;     34MB (    33 MiB) avg

Total process virtual memory:   3760MB (  3585 MiB) max;   3759MB (  3585 MiB) avg

analysis.entryFunction = run_service_maxrgb_cpu

analysis.programNames = preprocessed.c

analysis.traversal.order = DFS

ARGCPA.cpa = cpa.composite.CompositeCPA

CompositeCPA.cpas = cpa.location.LocationCPA, cpa.callstack.CallstackCPA, cpa.sign.SignCPA, cpa.interval.IntervalAnalysisCPA

coverage.enabled = false

cpa = cpa.PropertyChecker.PropertyCheckerCPA

cpa.callstack.domain = FLATPCC

cpa.callstack.skipRecursion = true

cpa.predicate.encodeBitvectorAs = INTEGER

cpa.predicate.encodeFloatAs = INTEGER

cpa.propertychecker.className = NoTargetStateChecker

limits.time.cpu = 900s

log.level = INFO

parser.usePreprocessor = true

pcc.proofFile = arg.proof

pcc.proofgen.doPCC = true

pcc.storeConfig = true

pcc.strategy = arg.ARG_CPAStrategy

PropertyCheckerCPA.cpa = cpa.arg.ARGCPA

solver.solver = SMTInterpol

specification = config/specification/default.spc

statistics.memory = true

1	/* service_maxrgb_cpu.c */
2
3	/* service_maxrgb.h */
4
5	#ifndef __SERVICE_MAXRGB_H__
6	#define __SERVICE_MAXRGB_H__
7
8	/* service_plugin.h */
9
10	#ifndef __SERVICE_PLUGIN_H__
11	#define __SERVICE_PLUGIN_H__
12
13	#include <stdint.h>
14
15	#define QuantumRange UINT16_MAX
16
17	typedef uint16_t Quantum;
18
19	typedef struct __PixelPacket__ {
20	Quantum blue;
21	Quantum green;
22	Quantum red;
23	Quantum opacity;
24	} PixelPacket;
25
26	typedef struct __Image__ {
27	PixelPacket *image;
28	int32_t rows;
29	int32_t columns;
30	int64_t j_arr;
31	} Image;
32
33	void run_service(char resource, void handler_gpu, Image target_images, int32_t target_images_size, Image source_images, int32_t source_images_size, double params, int32_t *status_code);
34
35	void get_service_ids(char **id_strings, int32_t id_strings_size);
36	void get_service_info(char **info_strings, int32_t info_strings_size);
37	void get_service_params(char **param_strings, int32_t param_strings_size);
38	void get_service_resources(char **resource_strings, int32_t resource_strings_size);
39	int32_t get_number_of_input_images(void);
40	int32_t get_number_of_output_images(void);
41
42	#endif /* __SERVICE_PLUGIN_H__ */
43	/* common.h */
44
45	#ifndef __COMMON_H__
46	#define __COMMON_H__
47
48	#include <stdio.h>
49
50	void malloc_copy_string_array(char *target_array, char source_array, int32_t array_size);
51	void free_string_array(char ***array, int32_t array_size);
52
53	#endif /* __COMMON_H__ */
54
55	#include <stdio.h>
56
57	int32_t run_service_maxrgb_scpu(PixelPacket pixpack_target, PixelPacket pixpack_source, int32_t rows, int32_t columns, int32_t mode);
58	int32_t run_service_maxrgb_cpu(PixelPacket pixpack_target, PixelPacket pixpack_source, int32_t rows, int32_t columns, int32_t mode);
59	int32_t run_service_maxrgb_gpu(PixelPacket pixpack_target, PixelPacket pixpack_source, int32_t rows, int32_t columns, int32_t mode);
60	int32_t run_service_maxrgb_fpga(PixelPacket pixpack_target, PixelPacket pixpack_source, int32_t rows, int32_t columns, int32_t mode);
61
62	// internal maxfile interface(s)
63	void run_service_max_maxrgb(uint16_t dataOut, uint16_t dataIn, uint32_t picSize, uint32_t mode);
64
65	#endif /* __SERVICE_MAXRGB_H__ */
66
67	int32_t run_service_maxrgb_cpu(PixelPacket pixpack_target, PixelPacket pixpack_source, int32_t rows, int32_t columns, int32_t mode) {
68	int32_t i, j, pos;
69
70	/**
71	* Modes:
72	* 1: maxRGB
73	* 2: minRGB
74	* 3: max increase
75	* 4: min erase
76	**/
77
78	if ((mode == 1) \|\| (mode == 3)) {
79	#pragma omp parallel
80	{
81	#pragma omp for private(j, pos)
82	for (i = 0; i < rows; ++i) {
83	for (j = 0; j < columns; ++j) {
84	pos = i * columns + j;
85
86	//check if color is grey
87	if ((pixpack_source[pos].red == pixpack_source[pos].green) && (pixpack_source[pos].red == pixpack_source[pos].blue)) {
88	pixpack_target[pos].red = pixpack_source[pos].red;
89	pixpack_target[pos].green = pixpack_source[pos].green;
90	pixpack_target[pos].blue = pixpack_source[pos].blue;
91	continue;
92	}
93
94
95	uint16_t *maxPtr;
96	maxPtr = &pixpack_source[pos].blue;
97	uint16_t *colorPtr;
98	colorPtr = &pixpack_source[pos].blue;
99	int8_t c;
100
101	for (c = 1; c < 3; c++) {
102	colorPtr++;
103	if (colorPtr > maxPtr)
104	maxPtr = colorPtr;
105	}
106
107	uint16_t *colorPtrSource;
108	colorPtrSource = &pixpack_source[pos].blue;
109	uint16_t *colorPtrTarget;
110	colorPtrTarget = &pixpack_target[pos].blue;
111
112	switch (mode) {
113	case 1:
114	for (c = 0; c < 3; c++) {
115	if (colorPtrSource == maxPtr)
116	colorPtrTarget = colorPtrSource;
117	else
118	*colorPtrTarget = 0;
119
120	colorPtrSource++;
121	colorPtrTarget++;
122	}
123	break;
124	case 3:
125	for (c = 0; c < 3; c++) {
126	if (colorPtrSource == maxPtr)
127	*colorPtrTarget = 65535;
128	else
129	colorPtrTarget = colorPtrSource;
130
131	colorPtrSource++;
132	colorPtrTarget++;
133	}
134	}
135	}
136	}
137	}
138	} else if ((mode == 2) \|\| (mode == 4)) {
139	#pragma omp parallel
140	{
141	#pragma omp for private(j, pos)
142	for (i = 0; i < rows; ++i) {
143	for (j = 0; j < columns; ++j) {
144	pos = i * columns + j;
145
146	//check if color is grey
147	if ((pixpack_source[pos].red == pixpack_source[pos].green) && (pixpack_source[pos].red == pixpack_source[pos].blue)) {
148	pixpack_target[pos].red = pixpack_source[pos].red;
149	pixpack_target[pos].green = pixpack_source[pos].green;
150	pixpack_target[pos].blue = pixpack_source[pos].blue;
151	continue;
152	}
153
154
155	uint16_t *minPtr;
156	minPtr = &pixpack_source[pos].blue;
157	uint16_t *colorPtr;
158	colorPtr = &pixpack_source[pos].blue;
159	int8_t c;
160
161	for (c = 1; c < 3; c++) {
162	colorPtr++;
163	if (colorPtr < minPtr)
164	minPtr = colorPtr;
165	}
166
167	uint16_t *colorPtrSource;
168	colorPtrSource = &pixpack_source[pos].blue;
169	uint16_t *colorPtrTarget;
170	colorPtrTarget = &pixpack_target[pos].blue;
171
172	switch (mode) {
173	case 2:
174	for (c = 0; c < 3; c++) {
175	if (colorPtrSource == minPtr)
176	colorPtrTarget = colorPtrSource;
177	else
178	*colorPtrTarget = 0;
179
180	colorPtrSource++;
181	colorPtrTarget++;
182	}
183	break;
184	case 4:
185	for (c = 0; c < 3; c++) {
186	if (colorPtrSource == minPtr)
187	*colorPtrTarget = 0;
188	else
189	colorPtrTarget = colorPtrSource;
190
191	colorPtrSource++;
192	colorPtrTarget++;
193	}
194	}
195	}
196	}
197	}
198	}
199	return 0;
200	}